Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
Identifieur interne : 005D07 ( Main/Exploration ); précédent : 005D06; suivant : 005D08Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
Auteurs : Frédéric BlanquiSource :
English descriptors
- KwdEn :
Abstract
Since Val Tannen's pioneer work on the combination of simply-typed lambda-calculus and first-order rewriting (LICS'88), many authors have contributed to this subject by extending it to richer typed lambda-calculi and rewriting paradigms, culminating in calculi like the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes induction-based definitions, is easier to write and provides more automation. On the other hand, checking that user-defined rewrite rules are strongly normalizing and confluent, and preserve the decidability of type-checking when combined with beta-reduction, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of ``sized types'' studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the later properties for a size algebra rich enough for capturing usual induction-based definitions and much more.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 004095
- to stream Crin, to step Curation: 004095
- to stream Crin, to step Checkpoint: 000155
- to stream Main, to step Merge: 005F30
- to stream Main, to step Curation: 005D07
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="621">Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations</title></titleStmt><publicationStmt><idno type="RBID">CRIN:blanqui05a</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">004095</idno><idno type="wicri:Area/Crin/Curation">004095</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004095</idno><idno type="wicri:Area/Crin/Checkpoint">000155</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000155</idno><idno type="wicri:Area/Main/Merge">005F30</idno><idno type="wicri:Area/Main/Curation">005D07</idno><idno type="wicri:Area/Main/Exploration">005D07</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>lambda-calculus</term><term>rewriting</term><term>size constraints</term><term>termination</term><term>typing</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="4630">Since Val Tannen's pioneer work on the combination of simply-typed lambda-calculus and first-order rewriting (LICS'88), many authors have contributed to this subject by extending it to richer typed lambda-calculi and rewriting paradigms, culminating in calculi like the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes induction-based definitions, is easier to write and provides more automation. On the other hand, checking that user-defined rewrite rules are strongly normalizing and confluent, and preserve the decidability of type-checking when combined with beta-reduction, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of ``sized types'' studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization. The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the later properties for a size algebra rich enough for capturing usual induction-based definitions and much more.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005D07 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005D07 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= CRIN:blanqui05a
|texte= Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
}}
| This area was generated with Dilib version V0.6.33. |  |